perm filename CONDIT[W77,JMC] blob
sn#272997 filedate 1977-03-28 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 .require "memo.pub[let,jmc]" source
C00013 00003 .skip 1
C00015 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.FONT B "MATH50"
.turn on "∂"
.cb CONDITIONAL EXPRESSIONS
The object of this note is to illustrate the mathematical uses of
conditional expressions as used in computer science. They are especially
convenient for defining and making formal calculations with functions
defined by different formulas on different parts of their domains. They
also provide a convenient domain-independent way of making a recursive
definitions, and they have a simple elementary theory which pleasantly
generalizes propositional calculus.
Conditional expressions have long been used in mathematics as the
right hand sides of definitions like
%2
.nofill
∂(15)x %1if%2 x ≥ 0,
!!a1: |x| =
∂(14)-x %1otherwise.
.fill
However, this doesn't make conditional expressions full mathematical
citizens, because they aren't used in mathematical sentences other
than definitions or as subexpressions.
The most common computer science notation for conditional
expressions is that of the programming
language Algol 60. In that notation, ({eq a1}) is written
!!a2: %2|x| = qif x ≥ 0 qthen x qelse -x%1.
It is customary to print the words qif, qthen and qelse in
bold face type and to singly underline them in handwriting or typescript.
A more compact but less mnemonic notation writes ({eq a1}) as
!!a3: %2|x| = (x ≥ 0 → x, -x)%1.
We will use the qif-qthen-qelse notation.
A simple conditional expression has the general form
!!a4: %2qif p qthen a qelse b%1
where ⊗p is an expression that can be true or false and ⊗a and ⊗b
take values in some domain ⊗D. Thus in ({eq a2}), ⊗a and ⊗b are
expressions whose values are real numbers. The value of ({eq a4})
is that of ⊗a if ⊗p is true and that of ⊗b if ⊗p is false. An
extended form of conditional expression
!!a5: %2qif p%41%2 qthen a%41%2 qelse qif p%42%2 qthen a%42%2
... qelse qif p%4n%2 qthen a%4n%2 qelse a%4n+1%1
is also used. Its value is that of %2a%4i%1, where ⊗i is the index
of the first of %2p%41%2_..._p%4n%1 that is true, and %2a%4n+1%1 if
none of the %2p%1's is true. The equation
!!a6: %2triangle(x) = qif x < -1 qthen 0 qelse qif x < 0 qthen 1 + x
qelse qif x < 1 qthen 1 - x qelse 0%1
defines the function graphed in figure 1.
.skip to column 1
.skip 25
.once center
Figure 1
Mathematical derivations are often easy to follow when they consist
of chains of equalities. Conditional expressions allow us to write chains
of equalities in place of a case analysis in an accompanying text.
Thus
.turn on "∂"
!!a6a: %2triangle(x) + triangle(1+x) =
= (qif x < -1 qthen 0 qelse qif x < 0 qthen 1+x
qelse qif x < 1 qthen 1-x qelse 0) + (qif 1+x < -1 qthen 0 qelse qif
1+x < 0 qthen 1+1+x qelse qif 1+x < 1 qthen 1-(1+x) qelse 0)
= (qif x < -2 qthen 0 qelse qif x < -1 qthen 0
qelse qif x < 0 qthen 1+x qelse qif x < 1 qthen 1-x qelse 0) +
(qif x < -2 qthen 0 qelse qif x < -1 qthen 2+x qelse qif x < 0 qthen -x
qelse qif x < 1 qthen 0 qelse 0)
= qif x < -2 qthen 0 qelse qif x < -1 qthen 2+x qelse qif x < 0
qthen 1 qelse qif x < 1 qthen 1-x qelse 0%1.
%3Recursion%1
A common use of conditional expressions in computer science
is for defining functions recursively. Thus we can define the factorial
function by
!!a7: %2n! ← qif n = 0 qthen 1 qelse n%8 * %2(n - 1)!%1,
where the symbol ← means that %2n!%1 is to be evaluated by evaluating
the right hand side of ({eq a7}), using ({eq a7}) whenever it is
necessary to evaluate a factorial.
In order to make such recursive definitions work, we must adhere to
the rule that if ⊗p is true we take ⊗a without evaluating ⊗b while
if ⊗p is false we evaluate ⊗b without evaluating ⊗a. Otherwise,
using ({eq a7}) to evaluate 0! would involve the
computation of (-1)! which would, following the definition, run
on forever.
The evaluation of 2! then takes the form
.nofill
!!a8: %22! = qif (2 = 0) qthen 1 qelse 2%8 * %2(2 - 1)!
= 2%8 * %21!
= 2%8 * %2(qif 1 = 0 qthen 1 qelse 1%8 * %2(1 - 1)!)
= 2%8 * %21%8 * %20!
= 2%8 * %21%8 * %2(qif 0 = 0 qthen 1 qelse 0%8 * %2(0 - 1)!)
= 2%1.
.fill
If we start from the successor function %2n'_=_n_+_1%1
the constant 0, and the equality predicate
and make a chain of recursive conditional expression definitions,
we get all
functions on the non-negative integers
that are computable by electronic computers (or by Turing machines).
Programs in the LISP language for computing with
symbolic expressions are defined by such conditional expression recursions.
(McCarthy 1963) and (McCarthy 1960) describe these matters.
The reader may try his hand at the recursive definition
!!a9: %2f(x) ← qif x > 100 qthen x - 10 qelse f(f(x + 11))%1
and show that the function it defines may also be written
!!a10: %2f(x) ← qif x > 100 qthen x - 10 qelse 91%1.
The function defined by
!!a11: %2f(x) ← qif x = 1 qthen 1 qelse qif 2|x qthen f(x/2) qelse f(3x + 1)%1
seems to always evaluate to 1, but no-one has been able to prove it.
.bb Theory of conditional expressions.
The theory of conditional expressions is a generalization of
propositional calculus in the following respect. Propositional functions
take the truth values ⊗T and ⊗F as arguments and have truth values as
values. Conditional expressions take truth values as arguments
but take their values in an arbitrary domain, e.g. the integers, real numbers
or symbolic expressions.
In the first place, if ⊗a and ⊗b are truth values, then
!!a12: %2qif p qthen a qelse b ≡ (p ∧ a) ∨ (¬p ∧ b)%1
so that when ⊗a and ⊗b are restricted to have ⊗T and ⊗F as values,
conditional expressions just give rise to
a ternary propositional connective - and one which was
studied before conditional expressions became popular. See (Church
1956). Conversely,
!!a13: %2p ∧ q ≡ qif p qthen q qelse F%1,
!!a14: %2p ∨ q ≡ qif p qthen T qelse q%1,
and
!!a15: %2¬p ≡ qif p qthen F qelse T%1.
We can form compound conditional expressions some of whose
terms are conditional expressions, and they satisfy identities like
!!a16: %2qif p qthen (qif q qthen a qelse b) qelse c = qif q qthen
(qif p qthen a qelse c) qelse (qif p qthen b qelse c)%1
Any candidate for such an identity can be checked by truth tables
in the same way a formula of propositional calculus can be checked to
see if it is a tautology.
There are also canonical forms for compound conditional expressions
analogous to those of propositional calculus, and there are algorithms
for transforming any compound conditional expression into any of these
canonical forms. Details are given in (McCarthy 1963).
There is also a useful distributive law, namely
!!a17: %2f(qif p qthen a qelse b) = qif p qthen f(a) qelse f(b)%1.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305
ARPANET: MCCARTHY@SU-AI
.end
.turn on "{"
%7This draft of
CONDIT[W77,JMC]
PUBbed at {time} on {date}.%1
.skip to column 1
Possible additional topics
1. undefined truth table and canonical forms
2. the generalized law of substitution of equals for equals
3. wffs and terms
4. more examples of conditional expressions
5. discussion of arguments by cases
6. Use of propositional connective for recursive definition and
the unsymmetrical connectives.